A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))
 (ma-interface-conds(I;i)
 ( k:Knd fp
 ( V:Type
 (  (State(if ma-interface-loc(I;i) then ma-interface-ds(I;i) else  fi )V(A + Top))) 

latex

Definitions

s = t, t  T, Type, MaInterface(T), Id, (x  l), A, x:A  B(x), b, Atom$n, a < b, x:A. B(x), x:AB(x), P  Q, False, left + right, ma-interface-locs(I), ma-interface-loc(I;i), , State(ds), Top, {x:A| B(x)} , x:A. B(x), strong-subtype(A;B), f  g, f(x)?z, P  Q, P & Q, P  Q, type List, x. t(x), loc(e), vartype(i;x), state@i, Namer(n;Id_list), State(ds), <a, b>, f(a), x  dom(f), {T}, True, T, ma-interface-ds(I;i), ma-interface-conds(I;i), ff, , , b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), p  q, p  q, p q, tt, , Unit, if b then t else f fi , Void, Knd, a:A fp B(a)

Lemmas

ifthenelse wf, l member wf, ma-interface-locs wf, Id wf, ma-interface wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, ma-interface-loc wf, bool wf, bnot wf, not wf, assert wf, ma-interface-conds wf2, ma-interface-conds wf, ma-interface-ds wf, fpf-trivial-subtype-top, true wf, squash wf, fpf wf, subtype-fpf2, Knd wf, member wf, top wf, decl-state wf, subtype rel wf